D:Dsys, sched:(Id((IdLnk+Id)+Unit)), v:(i:IdM(i).state),
dec:(i,a:IdM(i).state(M(i).da(locl(a))+Unit)).
Feasible(D)
 (i:Id, t:.
 (s:M(i).state.
 (s = if t=0 x.M(i).init(x)?v(i,x) else 1of(CV(d-comp(D;v;sched;dec))(t-1,i)) fi
 (& CV(d-comp(D;v;sched;dec))(t,i) = stutter-state(s)  d-world-state(D;i)
 (&  (k:Knd, val:d-decl(D;i)(k).
 (&  (CV(d-comp(D;v;sched;dec))(t,i) = next-world-state(D;i;s;k;val)  d-world-state(D;i)
 (&  (& isrcv(k)
 (&  (& & destination(lnk(k)) = i
 (&  (& & & ||queue(lnk(k);t)||1
 (&  (& & & & hd(queue(lnk(k);t)) = msg(lnk(k);tag(k);val)  Msg(l,tg. M(source(l)).dout(l,tg))
 (&  (&  islocal(k))) 

latex

Definitions

x:AB(x), s = t, Knd, d-decl(D;i), d-world-state(D;i), b, Id, ij, M.dout(l,tg), Msg(M), A & B, P & Q, left+right, P  Q, x:A. B(x), x:AB(x), Dsys, Feasible(D), {x:A| B(x) }, , x:A. B(x), hd(l), Unit, Type, IdLnk, locl(a), M.da(a), a<b, Void, P  Q, False, A, AB, , #$n, n-m, d-comp(D;v;sched;dec), CV(F), f(a), 1of(t), M(i), M.init(x)?v, x.A(x), i=j, if b t else f fi, M.state, t  T, {i..j}, Prop, b, , P  Q, State(ds), -n, n+m, S  T, i  j < k, S  T, let x = a in b(x), d-partial-world(D;f;t';s), World, queue(l;t), Msg, ||as||, destination(l), i = j, ij, p  q, True, i<j, p  q, T, P  Q, doact(k;v), mtag(m), rcv(l,tg), w.M, mval(m), {T}, tag(k), lnk(k), act(k), islocal(k), kindcase(k; a.f(a); l,t.g(l;t) ), w-action-dec(TA;M;i), a = b, mlnk(m), source(l), <a,b>, MsgA, stutter-state(s), msg(l;t;v), d-world(D;v;sched;dec), type List, isrcv(k), next-world-state(D;i;s;k;v), M.dout2(l;tg), d-comp-partial-world(D;v;sched;dec;t), s ~ t, SQType(T), M.ds(x), Dec(P), snds(l;t), rcvs(l;t), Case b of inl(x)  s(x) ; inr(y)  t(y), M.ef(k,x,s,v)?w, M.din(l,tg), M.Msg, M.sends(k,s,v), null, inr(x), f(x)?z

Lemmas

subtype rel list, filter type, mlnk wf d, ma-msg wf, ma-send-val wf, doact wf, d-decl-subtype, ma-ef-val wf, false wf, Knd sq, mtag wf, decidable int equal, d-comp-partial-world wf, w-queue-partial, ma-dout2 wf, mval wf, d-decl wf, next-world-state wf, isrcv wf, ge wf, Msg wf, d-world wf, msg wf, lnk wf, tagof wf, islocal wf, stutter-state wf, ma-dout wf, msga wf, lsrc wf, mlnk-hd-w-queue, assert-d-eq-Loc, assert-eq-id, eq id wf, not rcv locl, rcv one one, Knd wf, rcv wf, hd wf, assert of band, and functionality wrt iff, assert of lt int, bnot thru band, squash wf, true wf, bnot of lt int, assert of bor, or functionality wrt iff, assert of le int, band wf, lt int wf, bor wf, le int wf, d-eq-Loc wf, ldst wf, length wf1, w-Msg wf, w-queue wf, subtype rel self, world wf, d-partial-world wf, ifthenelse wf, CV wf, le wf, ma-init-val wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, not wf, assert wf, d-comp wf2, int seg wf, d-world-state wf, d-feasible wf, ma-da wf, locl wf, ma-st wf, d-m wf, nat wf, IdLnk wf, Id wf, unit wf, dsys wf, nat properties